 

 grammar mccproperty;



ID: 
  ('a'..'z'|'A'..'Z'|'0'..'9'|'_')+;


EOL:
  ('\r' | '\n')+;


INTEGER : [0-9]+;

identifier: ID;

property_set: property+;


mop : '&' | '|';
operator : 'I' | 'N' | 'A' | 'E' | 'G' | 'F';
ifs : '=>' | '<=>';
x : 'X';
xor : 'xor';
space: WS? ;
not : '!';
untils : 'U' | 'W'; 
integer : INTEGER+;
WS : [ \t\r\n]+ -> skip ; 


property: 
  ( 'reach' | 'struct' | 'ctl' | 'ltl' )? space identifier  ':' complex_formula space EOL
  ;

simple_formula_next : x integer? '~'? simple_formula;

simple_formula_liveness : identifier '?' ('l0' | 'l1' | 'l2' | 'l3' | 'l4')?;


simple_formula_comparer : complex_expression comparer complex_expression ;



simple_formula_const : 'true' | 'false' | 'deadlock';
simple_formula: space (
    simple_formula_const
  | '(' complex_formula ')'
  | not simple_formula
  | simple_formula_next
  | operator simple_formula
  | simple_formula_liveness
 | simple_formula_comparer
  ) space;

complex_formula:
 simple_formula  ( 
							   (mop  simple_formula)+
                                                         | (xor   simple_formula)
                                                         | (ifs simple_formula)
                                                         | (untils   simple_formula)
                                                         )?
  ;

algebra_operatorm : '+' | '*';
algebra_operator : '-' | '/';

complex_expression:
	simple_expression 
	( (algebra_operatorm simple_expression)+
    | (algebra_operator simple_expression)
    space )?
        ;

simple_expression:
  
   'bound' '(' identifier ')'
  | '|' complex_expression '|'
  | '<'anonymous_bindings'>'
  | 'marking' '(' identifier ')'
  | '(' complex_expression ')'
  | identifier
  ;


anonymous_bindings:
    identifier (',' identifier)*;

comparer : '=' | '!=' | '<' | '<=' | '>' | '>=';